Nuprl Definition : ma-interface-glued-p
11,40
postcript
pdf
ma-interface-glued-p(
es
;
A
;
I
;
l
;
tg
)
== ma-interface-consistent(
es
;
I
)
==
& (
e
:E. (kind(
e
) = rcv(
l
,
tg
))
(valtype(
e
)
r
A
))
==
& glued(
es
;
A
; (
e
.[[
I
]](
e
)); [[
I
]]; es-in-port(
es
;
l
;
tg
))
latex
clarification:
ma-interface-glued-p(
es
;
A
;
I
;
l
;
tg
)
== ma-interface-consistent(
es
;
I
)
==
& (
e
:es-E(
es
). (es-kind(
es
;
e
) = rcv(
l
,
tg
)
Knd)
(es-valtype(
es
;
e
)
r
A
))
==
& glued(
es
;
A
; (
e
.ma-abs-interface(
es
;
I
)(
e
)); ma-abs-interface(
es
;
I
); es-in-port(
es
;
l
;
tg
))
latex
Definitions
ma-interface-consistent(
es
;
X
)
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
E
,
P
Q
,
s
=
t
,
Knd
,
kind(
e
)
,
rcv(
l
,
tg
)
,
valtype(
e
)
,
glued(
es
;
B
;
f
;
Ia
;
Ib
)
,
x
.
A
(
x
)
,
X
(
e
)
,
[[
X
]]
,
es-in-port(
es
;
l
;
tg
)
FDL editor aliases
ma-interface-glued-p
origin